Step of Proof: p-fun-exp-add1-sq 11,40
Inference at * 1 2 2 
Iof proof for Lemma p-fun-exp-add1-sq:

.....falsecase..... NILNIL

1. A : Type
2. f : A(A + Top)
3. x : A
4. isl(f(x))
5. n : 
6. 0 < n
7. (primrec(n - 1;f o p-id()  ;i,g. f o g  )(x))
7. ~
7. (primrec(n - 1;p-id();i,g. f o g  )(outl(f(x))))
8. (n = 0)
  ((i,g. f o g  )((n - 1),primrec(n - 1;f o p-id()  ;i,g. f o g  ),x))
  ~
  ((i,g. f o g  )((n - 1),primrec(n - 1;p-id();i,g. f o g  ),outl(f(x)))) 
latex
 by (Reduce 0) 
CollapseTHEN ((RW (SubC (AddrC [1] (UnfoldTopAbC))) 0) 
CollapseTHEN ((RepUR ``
Ccan-apply do-apply`` ( 0)) 
CollapseTHEN (ProveSqEq))) 
latex

C.

Definitionsf o g  , can-apply(f;x), do-apply(f;x)

origin